(module expand-type (lib "eopl.ss" "eopl")

  (require "lang.scm")
  (require "static-data-structures.scm")

  (provide expand-type-in-tenv expand-module-type-in-tenv)
  (provide wrap-named-types-with-m-name)

;;;;;;;;;;;;;;;; expand-type-in-tenv ;;;;;;;;;;;;;;;;

  ;; expand-type-in-tenv expands a type until it contains no type
  ;; abbreviations. 

  ;; For example, if tenv contains a declaration for a module

  ;;   module m1
  ;;    interface
  ;;     [abstract-type t
  ;;      type-abbrev u = int
  ;;      type-abbrev v = (t -> u)]

  ;; then calling expand-type-in-tenv on from m1 take v should return
  ;; (from m1 take t -> int)  

  (define expand-type-in-tenv
    (lambda (ty tenv)
      (cases type ty
        (proc-type (arg-type result-type)
          (proc-type
            (expand-type-in-tenv arg-type tenv)
            (expand-type-in-tenv result-type tenv)))
        (named-type (name)
          (cond
            ((type-abbrev->maybe-binding-in-tenv name tenv)
             => (lambda (ty1) (expand-type-in-tenv ty1 tenv)))
            (else ty)))
        (qualified-type (m-name t-name)
          (expand-qualified-type-in-tenv m-name t-name tenv))
        (else ty)   ;; this covers int, bool, and tvar-types. 
        )))

  ;; this is the interesting case

  (define expand-qualified-type-in-tenv
    (lambda (m-name t-name tenv)
      (let ((ty (qualified-type m-name t-name)))
        (cond
          ((module-name->maybe-binding-in-tenv tenv m-name)
           => (lambda (m-type)
                (cases module-type m-type
                  (env-module-type (decls)
                    (cond
                      ((type-abbrev->maybe-binding-in-decls t-name decls)
                       =>
                       ;; yes, wrap any named types in
                       ;; qualified-type, and then continue to expand
                       (lambda (ty)
                         (expand-type-in-tenv
                           (wrap-named-types-with-m-name ty m-name)
                           tenv)))
                      (else ty)))
                  (else
                    (eopl:error
                      'type->maybe-binding-in-tenv
                      "Attempt to retrieve type from non-basic module ~s"
                      m-name)))))
          (else ty)))))

  ;; given a symbol, report its definition if it is defined as a
  ;; type-abbrev in tenv or #f if it is defined as an abstype or
  ;; undefined.  (Why not an error? That will somebody else's
  ;; responsibility). 

  (define type-abbrev->maybe-binding-in-tenv
    (lambda (search-sym tenv)
     (let recur ((tenv tenv)) 
        (cases type-environment tenv
          (empty-tenv () #f)
          (extend-tenv-with-type-abbrev (name ty saved-tenv)
            (if (eqv? name search-sym)
              ty
              (recur saved-tenv)))
          (extend-tenv-with-abstype (name saved-tenv) 
            (if (eqv? name search-sym)
              #f                        ; nope, it's bound abstractly
              (recur saved-tenv)))
          (else (recur (tenv->saved-tenv tenv))))
     )))

  ;; walk through the type wrapping named types in m-name

  (define wrap-named-types-with-m-name
    (lambda (ty m-name)
      (let recur ((ty ty))
        (cases type ty
          (int-type () ty)
          (bool-type () ty)
          (proc-type (arg-type result-type)
            (proc-type
              (recur arg-type)
              (recur result-type)))
          (named-type (ty-name) (qualified-type m-name ty-name))
          (qualified-type (modname varname) ty)
          (tvar-type (serial-number) 
            (eopl:error 'wrap-type-with-m-name
              "can't expand a tvar type ~s"
              ty))
            ))))

  (define expand-module-type-in-tenv
    (lambda (m-type tenv)
      (cases module-type m-type
        (proc-module-type
          (m-var m-type1 m-type2)
          (let ((expanded-m-type1
                  (expand-module-type-in-tenv m-type1 tenv)))
            (let ((expanded-m-type2
                    (expand-module-type-in-tenv m-type2
                      (extend-tenv-with-module
                        m-var expanded-m-type1 tenv))))
              (proc-module-type
                m-var expanded-m-type1 expanded-m-type2))))
        (env-module-type (decls)
          (env-module-type
            (expand-decls-in-tenv decls tenv))))))

  (define expand-decls-in-tenv
    (lambda (decls tenv)
      (map 
        (lambda (decl) (expand-decl-in-tenv decl tenv))
        decls)))

  (define expand-decl-in-tenv
    (lambda (decl tenv)
      (cases declaration decl
        (abstract-type-declaration (name) decl)
        (type-abbrev-declaration (name ty)
          (type-abbrev-declaration
            name
            (expand-type-in-tenv ty tenv)))
        (val-declaration (name ty)
          (val-declaration name 
            (expand-type-in-tenv ty tenv))))))

  ;; is search-sym bound to a *concrete* type in decls? If so, return
  ;; its RIGHMOST binding.  
  ;; by rights, this ought to be in lang.scm, but it's only called
  ;; from here.
  (define type-abbrev->maybe-binding-in-decls
    (lambda (search-sym decls)
      (linsearchr decls #f
        (lambda (decl)
          (cases declaration decl
            (type-abbrev-declaration (name ty)
              (if (eqv? name search-sym)
                ty
                #f))
            (else #f))))))

  )
